T:Type, l,l1,l2:(T List). iseg(T; l1; l)  iseg(T; l2; l)  compat(T; l1; l2) 

latex

Definitions	False, A, A  B, A c B, P  Q, P  Q, x:A. B(x), prop{i:l}, t  T, , decidable(P)
Lemmas	select wf, nat wf, length wf1, le wf, iseg wf, decidable le